package com.solver.demo.smt.main;

import cn.hutool.core.io.IoUtil;
import com.google.common.base.Ascii;
import lombok.extern.slf4j.Slf4j;
import org.sosy_lab.common.NativeLibraries;
import org.springframework.core.io.Resource;
import org.springframework.core.io.support.PathMatchingResourcePatternResolver;
import org.springframework.core.io.support.ResourcePatternResolver;

import java.io.File;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.util.Objects;
import java.util.concurrent.atomic.AtomicInteger;

@Slf4j
public class SmtLibLoadUtil {
    private static final ResourcePatternResolver resolver = new PathMatchingResourcePatternResolver();
    private static final AtomicInteger isLoaded = new AtomicInteger(0);

    public static synchronized void loadLibrary(String name) {
        if (isLoaded.get() == 2) {
//            log.info("z3本地库已加载");
            return;
        }
        try {
            Resource resource = getNativeLibraryResource(name);
            File file = copyLibrary(resource);
            loadLibrary(name, file);
            if (file != null) {
                isLoaded.getAndIncrement();
            }
        } catch (Exception e) {
            isLoaded.set(0);
            throw e;
        }
    }

    private static Resource getNativeLibraryResource(String name) {
        try {
            String osLibName = System.mapLibraryName(name);
            String arch = Ascii.toLowerCase(NativeLibraries.Architecture.guessVmArchitecture().name());
            String os = Ascii.toLowerCase(NativeLibraries.OS.guessOperatingSystem().name());
            if (NativeLibraries.OS.MACOSX.name().equalsIgnoreCase(os)) {
                arch = System.getProperty("os.arch");
            }
            Resource resource = getResource(os + "/" + arch + "/" + osLibName);
            if (resource != null) {
                log.info("加载z3本地库, name:{}, arch:{}, os:{}, osLibName:{}, resource:{}", name, arch, os, osLibName, resource.getURL());
                return resource;
            } else {
                resource = getResource(os + "/" + osLibName);
            }
            if (resource != null) {
                log.info("加载z3本地库, name:{}, arch:{}, os:{}, osLibName:{}, resource:{}", name, arch, os, osLibName, resource.getURL());
                return resource;
            } else {
                log.info("加载z3本地库, name:{}, arch:{}, os:{}, osLibName:{}, resource: 不存在", name, arch, osLibName, os);
                return null;
            }
        } catch (IOException e) {
            log.error("加载z3本地库失败", e);
        }
        log.info("加载z3本地库, name:{}, resource: 不存在", name);
        return null;
    }

    private static Resource getResource(String name) {
        try {
            Resource[] resources = resolver.getResources("classpath*:lib/" + name);
            if (resources.length > 0 && resources[0].exists()) {
                return resources[0];
            }
        } catch (IOException e) {
            log.error("加载z3本地库失败 name:{}, classpath*:lib", name, e);
        }
        return null;
    }

    private static File copyLibrary(Resource resource) {
        if (resource == null) {
            return null;
        }
        String tDir = System.getProperty("java.io.tmpdir");
        File tempFile = new File(tDir, Objects.requireNonNull(resource.getFilename()));
        try (InputStream inputStream = resource.getInputStream();
             FileOutputStream outputStream = new FileOutputStream(tempFile)) {
            IoUtil.copy(inputStream, outputStream);
            return tempFile;
        } catch (IOException e) {
            tempFile.deleteOnExit();
            log.error("加载z3本地库失败, 复制文件", e);
        }
        return null;
    }

    private static void loadLibrary(String name, File file) {
        if (file == null) {
            System.loadLibrary(name);
        } else {
            try {
                System.load(file.getAbsolutePath());
            } finally {
                file.deleteOnExit();
            }
        }
    }
}